\documentclass[a4paper,10pt]{article}
\usepackage[utf8x]{inputenc}
\usepackage{amssymb,amsmath}
\usepackage{graphicx}
\usepackage[linesnumbered]{algorithm2e}

\mathchardef\mhyphen="2D

\title{MAC5789\\
Laboratório de Inteligência Artificial\\
Projeto 1 - Resolvedores SAT\\
Prof. Marcelo Finger}
\author{Renato Urquiza Lundberg}

\begin{document}

\maketitle


\pagebreak

\section{Introdução}

Este relatório descreve o processo utilizado para realização de dois
experimentos propostos como primeiro projeto da disciplina de Laboratório de
Inteligência Artificial, assim como seus resultados.

O primeiro experimento consiste no levantamento da curva de mudança de fase para
o resolvedor \emph{SAT} \emph{MiniSAT}.

O segundo experimento exige que seja desenvolvida uma transformação polinomial
do problema do ciclo hamiltoniano para \emph{SAT}, tendo como finalidade o levantamento
de relações entre características do grafo e a probabilidade do mesmo possuir
ciclos hamiltonianos.

\pagebreak

\section{Metodologia}

Como o projeto foi bastante prático, e com grande preocupação com a corretude,
foi utilizada a metodologia de desenvolvimento \emph{Test Driven 
Development}, também conhecida como \emph{TDD}.

A metodologia determina que o desenvolvimento do programa deve ser feito
em ciclos curtos de desenvolvimento, que são iniciados com um teste que irá
induzir o desenvolvimento do programa principal propriamente dito.

Esses ciclos curtos e com início no teste trazem como benefício um design
obrigatoriamente modular, em que cada componente pode ser testado de forma
isolada.

Ao fim, quando todos os módulos são integrados, culminando no experimento, a
chance de ocorrerem problema é enormemente reduzida. Os resultados também são
mais confiáveis, pois cada trecho foi verificado automaticamente.

\pagebreak

\section{Curva de mudança de fase}

\subsection{SAT}

Também conhecido como \emph{Problema de Satisfatibilidade Booleana}, este
problema consiste em determinar se uma fórmula de lógica proposicional clássica
é ou não satisfatível.

Uma fórmula em lógica proposicional clássica é constituída de símbolos unidos
por conectivos. Os conectivos binários são $\vee$ indica disjunção lógica
(``ou'') e $\wedge$ conjunção lógica (``e''), $\neg$ é um conectivo unário que
denota negação lógica. Também são utilizados parênteses para definir a ordem
de execução das operações. Exemplo: $p \wedge \neg(q \vee r)$ pode ser lido
como ``p e não (q ou r)''.

Uma fórmula na lógica proposicional clássica é satisfatível se e somente se
existe um \emph{modelo lógico} para ela. Um modelo lógico é, de forma muito
resumida, uma intepretação $\mathcal{I}$ que atribua um valor \emph{verdadeiro}
ou \emph{falso} a cada símbolo e que satisfaça a fórmula (torne-a verdadeira).

Qualquer fórmula na lógica proposicional clássica pode ser transformada em
tempo polinomial em uma \emph{conjunção de disjunções}, esta forma é chamada
CNF, e pode ser obtida a partir de qualquer fórmula utilizando os seguintes
passos:

\begin{enumerate}
 \item Normalize negações, eliminando negações duplas e ``jogando a negação
para dentro''. Ex.: $\neg\neg x$ torna-se $x$ e $\neg(x \vee y)$ torna-se
$\neg x \wedge \neg y$.
 \item Distribua conjunções e disjunções.
\end{enumerate}

O experimento trata apenas de cláusulas na forma $CNF$, mas como qualquer fórmula
pode ser expressada nesta forma esta restrição não implica que estamos tratando
de alguma subconjunto potencialmente mais simples da lógica proposicional.

\subsection{MiniSAT}

O programa \emph{MiniSAT} é especializado em resolver o problema \emph{SAT}. Apesar
de pequeno, é extremamente eficiente, tendo ganhado em diversas categorias na
principal competição da área em 2005.

Seu uso é muito simples, como entrada deve ser passado um arquivo no formato
\emph{DIMACS}, muito comum na área e de fácil criação.

O resultado da execução apresenta diversos dados sobre a resolução, incluindo
contagens de eventos que ocorreram durante o processo, como conflitos. Também
é mostrado, claro, se a entrada é ou não satisfatível.

A integração com o \emph{MiniSAT} é feita através da chamada de um processo apartado,
seguido da leitura automatizada do resultado.

\subsection{Massa de testes}

A massa de testes, que deve conter milhares de exemplos de problemas de
satisfatibilidade, deve ser gerada. Cada problema consiste de uma fórmula com
100 átomos e um número pré-determinado de cláusulas de 3 literais.

Esta geração deve ser uniforme, ou seja, não deve haver tendência a gerar algum
determinado tipo de problema. Esse tipo de comportamento comprometeria o
experimento, dado que se trata de uma medição puramente estatística.

Para os testes é necessário criar um grafo aleatório com um número determinado
de variáveis e de cláusulas. Para tal é utilizado o seguinte procedimento:

\begin{enumerate}
 \item Crie o número desejado de cláusulas.
 \item Enquanto alguma variável não ocorrer em nenhuma cláusula (portanto o
problema no momento ainda não possui o número desejado de variáveis), uma
cláusula deve ser sorteada aleatoriamente para ser substituída por uma segunda,
que deve possuir ao menos a variável faltante.
\end{enumerate}

Afim de verificar que o algoritmo de geração estava correto, foram implementados
dois testes automatizados.

O primeiro garante que o problema gerado atende ao pedido: o número de átomos
utilizados é o pedido, possuem o número correto de cláusulas distintas, todas as
cláusulas possuem 3 literais. Este teste gera algumas dezenas de exemplares e
verifica todos.

O segundo garante a uniformidade da geração. São gerados um milhão de problemas
e a ocorrência de cada cláusula possível é contada. É então calculado o desvio
padrão das probabilidades de ocorrência de cada cláusula e verificado que este é
pequeno, portanto a geração é honesta, sem tendência a gerar determinada
cláusula.

\subsection{Experimento}

Uma vez que a integração com o \emph{MiniSAT} encontra-se segura, testada
automaticamente, e a geração da massa de dados correta e honesta, a modelagem do
experimento torna-se muito mais simples.

Como pedido, o número de variáveis é fixo ($N = 100$). Primeiro é calculado o
percentual de satisfatibilidade para $M/N$ de $1$ a $8$, sempre gerando 200
amostras para cada ponto. Em seguida é realizada uma busca binária, partindo do
intervalo que parece conter a mudança de fase, quando o percentual de
satisfatibilidade é $50\%$. Como estamos lidando com um $N$ fixo, não é possível
chegar ao ponto exato de mudança de fase, pois isso implicaria em um número
fracionário de cláusulas, o que é impossível.

Segue abaixo a saída da execução do experimento:

\begin{verbatim}
Medição feita para problemas de 100 variáveis e 100 cláusulas: 1.0
Medição feita para problemas de 100 variáveis e 200 cláusulas: 1.0
Medição feita para problemas de 100 variáveis e 300 cláusulas: 1.0
Medição feita para problemas de 100 variáveis e 400 cláusulas: 0.935
Medição feita para problemas de 100 variáveis e 500 cláusulas: 0.01
Medição feita para problemas de 100 variáveis e 600 cláusulas: 0.0
Medição feita para problemas de 100 variáveis e 700 cláusulas: 0.0
Medição feita para problemas de 100 variáveis e 800 cláusulas: 0.0
Medição feita para problemas de 100 variáveis e 450 cláusulas: 0.21
Medição feita para problemas de 100 variáveis e 425 cláusulas: 0.62
Medição feita para problemas de 100 variáveis e 437 cláusulas: 0.375
Medição feita para problemas de 100 variáveis e 431 cláusulas: 0.455
Medição feita para problemas de 100 variáveis e 428 cláusulas: 0.555
Medição feita para problemas de 100 variáveis e 429 cláusulas: 0.485
Mudança de fase entre 428 cláusulas (0.555) e 429 cláusulas (0.485)
\end{verbatim}


O resultado pode ser visto no seguinte gráfico:


\begin{figure}[h]
\begin{center}
 \includegraphics[scale=0.5]{curvaMudancaFase.png}
\end{center}
\end{figure}

A mudança de fase ocorre, portanto quando $M/N$ está entre 4,28 e 4,29.

Também foi observado que o resultado do programa variava entre execuções. Isso
se dá por que a semente dos números pseudo-aleatórios utilizados varia, tornando
sua execução não determinística. Além disso, 200 amostras é um número muito
pequeno para definir com precisão o percentual de satisfatibilidade. A execução
do experimento com um número maior de amostras por ponto resultou em resultados
mais precisos, não apresentando variações significativas entre execuções.

Segue abaixo a saída da execução do experimento, com 100.000 amostras por ponto.

\begin{verbatim}
Medição feita para problemas de 100 variáveis e 100 cláusulas: 1.0
Medição feita para problemas de 100 variáveis e 200 cláusulas: 1.0
Medição feita para problemas de 100 variáveis e 300 cláusulas: 1.0
Medição feita para problemas de 100 variáveis e 400 cláusulas: 0.92439
Medição feita para problemas de 100 variáveis e 500 cláusulas: 0.00459
Medição feita para problemas de 100 variáveis e 600 cláusulas: 0.0
Medição feita para problemas de 100 variáveis e 700 cláusulas: 0.0
Medição feita para problemas de 100 variáveis e 800 cláusulas: 0.0
Medição feita para problemas de 100 variáveis e 450 cláusulas: 0.18534
Medição feita para problemas de 100 variáveis e 425 cláusulas: 0.56938
Medição feita para problemas de 100 variáveis e 437 cláusulas: 0.36196
Medição feita para problemas de 100 variáveis e 431 cláusulas: 0.46403
Medição feita para problemas de 100 variáveis e 428 cláusulas: 0.5164
Medição feita para problemas de 100 variáveis e 429 cláusulas: 0.49744
Mudança de fase entre 428 cláusulas (0.5164) e 429 cláusulas (0.49744)
\end{verbatim}

\pagebreak

\section{Ciclos hamiltonianos}

\subsection{O Problema}

O problema dos ciclos hamiltonianos consiste em, dado um grafo, determinar se
existe um caminho (sequência de vértices vizinhos) que passe por cada um dos
vértices uma única vez, voltando no vértice inicial.

O estudo deste problema é de grande interesse da comunidade científica, pois é
um problema $NP\mhyphen completos$, ou seja, qualquer problema em $NP$ pode
ser reduzido polinomialmente a este.

\subsection{Conversão para SAT}

Assim como o problema do ciclo hamiltoniano é $NP\mhyphen completos$, $SAT$
também o é, portanto existe um algoritmo polinomial que transforma um problema
de existência de ciclo hamiltoniano em um problema de satisfatibilidade tal que
o problema de satisfatibilidade é satisfatível se e somente se o grafo original
possui ciclo hamiltoniano.

Utilizando esta transformação, podemos resolver o problema do ciclo hamiltoniano
utilizando um resolvedor \emph{SAT}, como o \emph{MiniSAT}.

Esta transformação utiliza como símbolos variáveis no formato $p_{ij}$ para
denotar que o $i$-ésimo vértice está na $j$-ésima posição do caminho.

\begin{enumerate}
 \item Cada vértice está em ao menos um ponto no caminho. Para cada vértice $i$
criar uma cláusula $\bigvee_{j \in path}{p_{ij}}$.
 \item Cada vértice ocorre no máximo uma vez no caminho. Para cada vértice $i$ e
para cada duas posições no caminho $j_1$ e $j_2$ criar uma cláusula
$\neg p_{ij_1} \vee \neg p_{ij_2}$.
 \item Cada posição do caminho possui ao menos um vértice. Para cada ponto $j$
no caminho criar uma cláusula $\bigvee_{i \in vertexes}{p_{ij}}$.
 \item Vértices em posições consecutivas no caminho devem ser vizinhos. Para
cada duas posições consecutivas no caminho $j_1$ e $j_2$, para cada dois
vértices não vizinhos $i_1$ e $i_2$, criar uma cláusula $\neg p_{i_1j_1} \vee
\neg p_{i_2j_2}$.
 \item O primeiro vértice está na primeira posição no caminho: $p_{00}$.
\end{enumerate}

O último item é dispensável à corretude da transformação, mas diminui
consideravelmente o espaço de busca, aumentando a eficiência do resolvedor.

Esta conversão é testada automaticamente através da conversão de 5 grafos
feitos manualmente, com resultado conhecido. Também é feito um teste que gera
50 grafos aleatórios e verifica a existência de ciclo hamiltoniano utilizando a
conversão para \emph{SAT} e um método convencional de busca em profundidade,
verificando que o resultado é sempre o mesmo.

\subsection{Massa de testes}

Para obter uma massa de testes para este experimento foi necessário gerar de
forma eficiente grafos aleatórios que possuissem 50 vértices com um grau fixo
pré-determinado.

A abordagem óbvia, de simplesmente sortear arestas a serem adicionadas, não
funciona sempre, chegando em um ponto em que não é mais possível adicionar
arestas e nem todos os vértices possuem o grau desejado. Após alguma pesquisa
cheguei ao algoritmo de Steger-Wormald, proposto em 97, que é de simples
implementação e gera grafos uniformes. Sua eficiência é bastante aceitável,
apesar de necessitar reinicializações. Para graus pequenos a reinicialização
é bem rara, mas para graus maiores torna-se muito frequente, chegando até mesmo
a serem necessárias milhares de reinicializações para gerar um único grafo.

Foi feito um teste que garante que os grafos gerados atendem ao
pedido: possuem o número pedido de vértices e todos os vértices possuem o grau
pedido. Também foi feito um teste que verifica a uniformidade dos grafos
gerados, verificando se o desvio padrão da probabilidade de cada aresta aparecer
no grafo é pequeno.

\subsection{Experimento}

Com a geração da massa de testes correta e a conversão bem testada, o
experimento tornou-se muito mais simples.

O experimento consiste em sortear grafos de 50 vértices com graus fixos, para
graus variando de 5 em 5.

Segue abaixo a saía do experimento realizado:

\begin{verbatim}
Degrees: 5 Satisfiability: 1.0 Average time: 5.898069275000001
Degrees: 10 Satisfiability: 1.0 Average time: 0.06622374499999995
Degrees: 15 Satisfiability: 1.0 Average time: 0.04716255499999994
Degrees: 20 Satisfiability: 1.0 Average time: 0.04398235
Degrees: 25 Satisfiability: 1.0 Average time: 0.042402255
Degrees: 30 Satisfiability: 1.0 Average time: 0.04184223000000001
Degrees: 35 Satisfiability: 1.0 Average time: 0.041622244999999974
Degrees: 40 Satisfiability: 1.0 Average time: 0.040442165
Degrees: 45 Satisfiability: 1.0 Average time: 0.04054217
\end{verbatim}	

Todos os grafos gerados possuíam ciclos hamiltonianos, mas o tempo para se
encontrar o ciclo foi significativamente maior para grafos de grau 5.
Possivelmente isso se dá pois um ciclo é mais difícil de ser encontrado, por
existirem menos ciclos.

O gráfico abaixo mostra a relação do tempo de execução com o grau dos vértices.
A escala utilizada é logarítmica, com base 10.

\begin{figure}[h]
\begin{center}
 \includegraphics[scale=0.5]{tempoExecucao.png}
\end{center}
\end{figure}

O gráfico abaixo mostra a relação do percentual de satisfatibilidade, grafos
com ciclos hamiltonianos, com o grau dos vértices.

\begin{figure}[h]
\begin{center}
 \includegraphics[scale=0.5]{percentualSatisfatibilidade.png}
\end{center}
\end{figure}

Foi feito também um experimento extra, com grafos de grau 1 até 49. A motivação
foi identificar em que ponto os grafos passam a conter sempre ciclos
hamiltonianos. Segue a saída:

\begin{verbatim}
Degrees: 1 Satisfiability: 0.0 Average time: 0.034481805
Degrees: 2 Satisfiability: 0.25 Average time: 0.041742219999999976
Degrees: 3 Satisfiability: 1.0 Average time: 368.40710626000015
Degrees: 4 Satisfiability: 1.0 Average time: 56.88461004
Degrees: 5 Satisfiability: 1.0 Average time: 5.546966894999998
Degrees: 6 Satisfiability: 1.0 Average time: 1.0552856349999997
Degrees: 7 Satisfiability: 1.0 Average time: 0.31681941
Degrees: 8 Satisfiability: 1.0 Average time: 0.1409084149999999
Degrees: 9 Satisfiability: 1.0 Average time: 0.08762513499999992
Degrees: 10 Satisfiability: 1.0 Average time: 0.0708040749999999
Degrees: 11 Satisfiability: 1.0 Average time: 0.06292355499999998
Degrees: 12 Satisfiability: 1.0 Average time: 0.05870330999999994
Degrees: 13 Satisfiability: 1.0 Average time: 0.055303079999999956
Degrees: 14 Satisfiability: 1.0 Average time: 0.05220285999999991
Degrees: 15 Satisfiability: 1.0 Average time: 0.051042829999999956
Degrees: 16 Satisfiability: 1.0 Average time: 0.05094281999999994
Degrees: 17 Satisfiability: 1.0 Average time: 0.05070281999999992
Degrees: 18 Satisfiability: 1.0 Average time: 0.04810267999999991
Degrees: 19 Satisfiability: 1.0 Average time: 0.0495027349999999
Degrees: 20 Satisfiability: 1.0 Average time: 0.04840266499999995
Degrees: 21 Satisfiability: 1.0 Average time: 0.0485626499999999
Degrees: 22 Satisfiability: 1.0 Average time: 0.04602251499999993
Degrees: 23 Satisfiability: 1.0 Average time: 0.04796261499999996
Degrees: 24 Satisfiability: 1.0 Average time: 0.04684249499999995
Degrees: 25 Satisfiability: 1.0 Average time: 0.04572248499999995
Degrees: 26 Satisfiability: 1.0 Average time: 0.050362744999999966
Degrees: 27 Satisfiability: 1.0 Average time: 0.048262610000000004
Degrees: 28 Satisfiability: 1.0 Average time: 0.04744257999999995
Degrees: 29 Satisfiability: 1.0 Average time: 0.04638252499999997
Degrees: 30 Satisfiability: 1.0 Average time: 0.046762544999999996
Degrees: 31 Satisfiability: 1.0 Average time: 0.04496238499999996
Degrees: 32 Satisfiability: 1.0 Average time: 0.044742415000000015
Degrees: 33 Satisfiability: 1.0 Average time: 0.04428239499999994
Degrees: 34 Satisfiability: 1.0 Average time: 0.045862474999999986
Degrees: 35 Satisfiability: 1.0 Average time: 0.04300233499999999
Degrees: 36 Satisfiability: 1.0 Average time: 0.046182554999999965
Degrees: 37 Satisfiability: 1.0 Average time: 0.041142205
Degrees: 38 Satisfiability: 1.0 Average time: 0.04170225
Degrees: 39 Satisfiability: 1.0 Average time: 0.04128220500000001
Degrees: 40 Satisfiability: 1.0 Average time: 0.042442285
Degrees: 41 Satisfiability: 1.0 Average time: 0.04154223500000001
Degrees: 42 Satisfiability: 1.0 Average time: 0.038862045
Degrees: 43 Satisfiability: 1.0 Average time: 0.04088216999999998
Degrees: 44 Satisfiability: 1.0 Average time: 0.04176224000000002
Degrees: 45 Satisfiability: 1.0 Average time: 0.04572242999999999
Degrees: 46 Satisfiability: 1.0 Average time: 0.04146220500000001
Degrees: 47 Satisfiability: 1.0 Average time: 0.044182369999999985
Degrees: 48 Satisfiability: 1.0 Average time: 0.039602120000000046
Degrees: 49 Satisfiability: 1.0 Average time: 0.038922030000000024
\end{verbatim}

Interessantemente, ocorreu um grande salto. Nenhum grafo de grau 1, obviamente,
possui ciclo, 25\% com grau 2 possuem ciclos, e para todos os graus maiores
praticamente 100\% dos grafos possuem ciclos hamiltonianos. O tempo também chama
atenção, para grau 3 a dificuldade do resolvedor em determinar a
satisfatibilidade do problema é enorme, levando diversos minutos por instância.
Esse tempo cai rapidamente com o aumento do grau, o que faz com que encontrar 
a solução torne-se mais fácil. O tempo de execução deste último experimento não
pode ser considerado muito preciso, infelizmente, pois os testes foram
executados em paralelo.

\section{Conclusão}

A realização dos experimentos evidenciou diversos pontos interessantes:

É fundamental a preocupação com a uniformidade das amostras. Não foi fornecida
prova teórica da corretude da geração, mas o teste empírico, analisando as
próprias amostras geradas pela implementação, dá uma boa confiança nos
resultados. Sem uma evidência de que as amostras não são viciadas, não é
possível acreditar nos resultados dos experimentos.

O número de execuções influencia, e muito, na precisão dos resultados. Quando o
número de amostras por ponto é pequena o resultado do experimento oscila
consideravelmente entre execuções. Este fenômeno ocorre com menos frequência
quando o número de amostras por ponto é elevado.

A velocidade nos experimentos é outro fator que fez diferença. A geração das
amostras tem que ser eficiente para possibilitar os testes. Outro ponto que
auxiliou muito foi a execução em paralelo dos testes. Infelizmente este último
recurso não pôde ser utilizado para os testes de tempo de execução, pois neste
caso a execução de uma instância influenciaria no tempo de execução da outra.

\end{document}